xxbasic, basic
\\[0ex]refl($T$;$E$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Refl($T$;$x$,$y$.$E$($x$,$y$))